Model checking is a method of formal verification that is gaining in popularity as a tool for use in designing complex systems, such as integrated circuits. The method is described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference.
To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φ} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that M |=φ, under all relevant input sequences. Such testing is a form of reachability analysis.
One of the most useful features of model checking is its ability, when a property φ is found to be false on M, to construct a sequence of states and transitions (a path) that leads to the problematic state of the design. This path is called a counterexample. It can be used by the engineer in understanding and remedying the design defect that led to the failure of the model.
Model checking is preferably carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993), which is incorporated herein by reference. A number of practical model checking tools are available, among them RuleBase, developed by IBM Corporation. This tool is described by Beer et al. in “RuleBase: an Industry-Oriented Formal Verification Tool,” in Proceedings of the Design Automation Conference DAC′96 (Las Vegas, Nev., 1996), which is incorporated herein by reference.
Symbolic CTL model checking as described by McMillan involves computing the transition-relation (TR) of the model, and then applying the model checking algorithm to verify a given formula. In many cases, the full TR is too big to be computed. This problem is addressed by Beer et al., in “On-the-fly Model Checking of RCTL Formulas,” Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 1998), which is incorporated here in by reference. In this paper, the authors describe a technique for solving CTL formulas of the form AG(p) on the fly, wherein p is a Boolean expression. An AG(p) formula states that p is true in every reachable state of the model. Therefore, to disprove this formula, it is sufficient to find one “bad” state in which p is false.
If S is the set of states in which p is false, then in order to find a bad state, it is necessary only to intersect S with the set of reachable states R, and check that the intersection is not empty. Finding this intersection is computationally easy, and therefore can be performed on the fly, i.e., after each iteration of the reachability analysis. If the intersection of S and R is found at any point to be non-empty, the process is stopped, and AG(p) is false. Otherwise, the process continues and terminates when the entire reachable state space has been computed, so that AG (p) is shown to be true. Thus, this method eliminates the large expenditure of computation resources needed to compute the full transition relation. Furthermore, since counterexamples are produced on the fly, only a portion of the reachable state space must be computed when the formula fails, saving even more time and memory space.
The on-the-fly model checking procedure is shown formally in Table I below:
TABLE ION-THE-FLY MODEL CHECKING1reachable = new = initialStates;2i = 0;3while ((new ≠ Ø) && (new ∩ p = Ø)) {4Si = new;5i = i+1;6next = nextStateImage (new)7new = next \ reachable;8reachable = reachable ∪ next;9}10if (new = Ø) {11print “formula is true in the model”;12return;13}Here the “&&” operator represents logical conjunction, and the function “nextStateImage(new)” returns the states that are reached in one cycle of the system transition relation beginning from the states in {new}.
In the above-mentioned article, Beer et al. also define a specification language RCTL, as a subset of the conventional CTL language using regular expressions. RCTL makes it possible to translate many CTL formulas conveniently into state machines having an error state. Such formulas can then be verified by on-the-fly model checking of the formula AG(error). More recently, Beer et al. have extended RCTL to include further expressions and syntax that are useful in creating formulas for on-the-fly model checking, as described in “The Temporal Logic Sugar,” Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001), which is incorporated here in by reference.